(* $Id: automaticProver.ml 218 2009-03-06 09:40:54Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

open XCoreSyntax

let ergo with_split dir (f, (q, _)) =
    (* FIXME: Ergo is not capable of deducing False from inconsistent
       hypothesis. *)
    if f.fvalue = FFalse then
      Ergo.inconsistent_assumptions q dir
    else Ergo.prove with_split q dir

let simplify dir (_, (_, q)) =
  Simplify.prove q

let trivial_prover dir (f, _) =
  TrivialProver.prove f

let rec try_with_provers dir failed_filenames query = function
  | [] -> (false, failed_filenames)
  | prover :: others ->
      let (ret, filename) = prover dir query in
	if not ret then
	  try_with_provers dir (filename :: failed_filenames) query others
	else
	  (ret, [filename])

let tries = ref 0
let success = ref 0

let prove f (env, ef) dir =
  incr tries;
  let filter = function Some "split" -> true | _ -> false in
  let try_ with_split q =
    try_with_provers dir
      []
      (f, q)
      [
        trivial_prover;
        ergo with_split;
        simplify;
      ]
  in
    (* Inconsistency proofs often require splitting. *)
    if ef = PFOLSyntax.PFalse then
      let ret' = try_ true (PFOLEnv.proof_obligation_to_query env ef) in
        if not (fst ret') then
          (false, snd ret')
        else
          (incr success; ret')
    else
      let ret =
        (* Most of the time, some axioms (about ADTs) are not useful but
           slowdown the automatic provers. *)
        try_ false (PFOLEnv.proof_obligation_to_query ~filter env ef)
      in
        if not (fst ret) then
          let ret' = try_ true (PFOLEnv.proof_obligation_to_query env ef) in
            if not (fst ret') then
              (false, snd ret @ snd ret')
            else
              (incr success; ret')
        else
          (incr success; ret)

let print_stats () =
  Printf.printf "[%d proofs over %d requests]\n" !success !tries
